Nuprl Lemma : upto_wf
11,40
postcript
pdf
n
:
. upto(
n
)
(int_seg(0;
n
) List)
latex
Definitions
t
T
,
int_seg(
i
;
j
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
subtype(
S
;
T
)
,
lelt(
i
;
j
;
k
)
,
P
Q
,
A
B
,
A
,
False
,
prop{i:l}
Lemmas
int
seg
wf
,
le
wf
origin
n:
. upto(n) 
(int_seg(0; n) List) n:. upto(n) (int_seg(0; n) List) Tx:A. B(x)
Q
Q
B
A